es:ES, ff:FIFO, is_req, is_ack:(E), awaiting, owes_ack:(IdIdId).
(ff.C r Id)
 (i, j:ff.C. @i(awaiting(i,j):) & @i(owes_ack(i,j):))
 (i:ff.C, e:E. (ff.R(i,e))  (loc(e) = i  Id))
 (e:E. Dec(is_req(e)) & Dec(is_ack(e)))
 (i, j:ff.C, e:E. Dec(ff.S(i,j,e)))
 (i, j:ff.C, e:E. (ff.S(i,j,e))  (loc(e) = i  Id))
 plus-ify{i:l}(es;ff;is_req;is_ack;awaiting;owes_ack)
 (sndr, rcvr:ff.C, e:E.
 [e: rcvr is_ack sndr]  (x:E. ((x <loc e) & [x: rcvr is_req sndr]))) 

latex

Definitions	(e <loc e'), A, if b then t else f fi , b, tt, {T}, SQType(T), e loc e' , P  Q, x:A. B(x), @i(x:T), A c B, @i x initially v:T, t  T, P & Q, P  Q, , x:A. B(x), x  {FDLNOr12445}, False, P  Q, Dec(P), plus-ify{i:l}(es;ff;is_req;is_ack;awaiting;owes_ack)
Lemmas	rcv-it wf, inconsistent-bool-eq, es-after wf, es-causl wf, es-locl-iff, es-loc-pred, es-le-loc, Id sq, es-when wf, es-locl wf, bnot wf, es-initially wf, decidable equal bool, es-vartype wf, es-isconst wf, assert wf, es-lc-bool, snd-it-loc, event system wf, FIFO wf, bool wf, es-dtype wf, fifoR wf, decidable wf, es-loc wf, Id wf, fifoS wf, plus-ify wf, fifoC wf, es-E wf, snd-it wf